Rframe(${\it loc}$; $T$; $x$; $L$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr inr inr (inl $<$${\it loc}$, $T$, $x$, $L$$>$ )